Example 6.9 in [Lucas - ENTCS64]

Summary: Ex6_9_Luc02c

• CS-TRS format
• OBJ format
• Negative results:
  1. Lucas' transformation (Extra variables)
• Positive results:
  1. Zantema's transformation (MuTerm)
  2. Ferreira and Ribeiro's transformation (MuTerm)
  3. Giesl and Middeldorp's transformation (Corollary)

CS-TRS Ex6_9_Luc02c (file Ex6_9_Luc02c.csr)

Functions:  2nd cons from s cons1

Constructors:  cons s cons1

Variables:  X Y Z X1

Arities: 

ar(2nd) = 1
ar(cons) = 2
ar(from) = 1
ar(s) = 1
ar(cons1) = 2

Replacement map: 

µ(2nd)={1}
µ(cons)={1}
µ(from)={1}
µ(s)={1}
µ(cons)={1,2}

Rules:  (file Ex6_9_Luc02c)   

2nd(cons1(X,cons(Y,Z))) -> Y
2nd(cons(X,X1)) -> 2nd(cons1(X,X1))
from(X) -> cons(X,from(s(X)))

The CS-TRS in OBJ format (file Ex6_9_Luc02c.obj):

obj Ex6_9_Luc02c is
  sort S .
  op 2nd : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op from : S -> S .
  op s : S -> S .
  op cons1 : S S -> S .
  vars X Y Z X1 : S .
  eq 2nd(cons1(X,cons(Y,Z))) = Y .
  eq 2nd(cons(X,X1)) = 2nd(cons1(X,X1)) .
  eq from(X) = cons(X,from(s(X))) .
endo

Negative results

1. The µ-termination of Ex6_9_Luc02c cannot be proved by using Lucas' transformation. The TRS Ex6_9_Luc02c_L:

       2nd(cons1(X,cons(Y))) -> Y
       2nd(cons(X)) -> 2nd(cons1(X,X1))
       from(X) -> cons(X)
       

   contains extra variables.

Positive results

1. The µ-termination of Ex6_9_Luc02c can be proved by using Zantema's transformation. The TRS Ex6_9_Luc02c_Z:

       2nd(cons1(X,cons(Y,Z))) -> Y
       2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
       from(X) -> cons(X,n__from(s(X)))
       from(X) -> n__from(X)
       activate(n__from(X)) -> from(X)
       activate(X) -> X
       

   is terminating (use MuTerm).
2. The µ-termination of Ex6_9_Luc02c can be proved by using Ferreira and Ribeiro's transformation. The TRS Ex6_9_Luc02c_FR:

       2nd(cons1(X,cons(Y,Z))) -> Y
       2nd(cons(X,X1)) -> 2nd(cons1(X,activate(X1)))
       from(X) -> cons(X,n__from(n__s(X)))
       from(X) -> n__from(X)
       s(X) -> n__s(X)
       activate(n__from(X)) -> from(activate(X))
       activate(n__s(X)) -> s(activate(X))
       activate(X) -> X
       

   is terminating (use MuTerm).
3. By [GM04, Theorem 22], the µ-termination of Ex6_9_Luc02c can also be proved by using Giesl and Middeldorp's transformation (but no concrete proof has been reported yet).